The present invention relates generally to the field of Computer-aided design (CAD) systems and methods, and more particularly to CAD systems and methods for digital circuit verification of sequential circuits.
Computer-aided design of digital circuits and other complex digital systems is widely prevalent. The requirements of the circuit or system are defined in an abstract model of the circuit or system. The abstract model is then successively transformed into a number of intermediate stages.
The design of the circuit or system therefore proceeds from the general requirements level to the lower detailed level of the physical design. Interposed between are a number of intermediate levels. These intermediate stages often include a register transfer level model which represents a block structure behavioral design, and a structural model which is a logic level description of the system. Each successive level of the design is tested or verified to ensure that the circuit or system continues to meet the designed specifications.
These circuits or systems may be divided, among other ways, into combinational circuits and sequential circuits. The outputs of a combinational circuit depend entirely on the value of the inputs to the circuit. Thus, the outputs of a combinational circuit do not depend on the values of previous inputs applied to the circuit. The outputs of sequential circuits, however, depend on past values of the inputs with the outputs dependent on the inputs to the circuit and previously generated values of the outputs or some node within the circuit. Thus, a sequential circuit may be viewed as a plurality of combinational logic elements with some of the outputs of the plurality of combinational logic fed back to some of the inputs of the combinational logic via storage elements.
An example of combinational logic is a series of interconnected AND gates in which none of the outputs of the AND gates are fed back to previous AND gates. An example of a storage element is a clocked flip-flop. Other examples of a storage element are latches, registers, and other similar types of storage devices. Initially storage elements have unknown values and need to be forced to specific known states. These known states depend on the inputs to the circuit, i.e., the primary inputs, and the present state of the storage elements. Thus, a sequential circuit may generate different output values for the same set of input vectors depending on the boolean values of the storage elements. Therefore, design verification of a sequential circuit is often complex.
Conventionally, design verification is accomplished by simulating the circuit or system. This is done by stimulating the circuit with a set of test vectors, which represent a set of appropriately chosen inputs to the circuit, and thereafter examining the outputs of the circuit. However, for many circuits that are large and complicated, extensive simulation of the circuit is impractical. Hence, other techniques for verifying sequential circuits have also been developed, such as a Boolean Decision Diagram (BDD) based state space traversal technique, and automatic test pattern generator (ATPG) based traversal technique.
The BDD based state traversal technique however, often requires space, i.e., memory space, which is exponential in the number of primary inputs to the circuit or system. Therefore, for many large circuits memory explosion is a problem. Similarly, the ATPG based traversal technique is inefficient if the circuit is too large.
However, the verification of sequential circuits may be simplified by determining correspondences between storage elements of the two circuits. If such correspondence can be determined the verification step is simplified to a verification step for combinational circuits. Therefore, especially for large circuits, determining the correspondence between the storage elements of the circuits is desirable. Conventional techniques to determine the correspondence between the storage elements, however, are often ineffective. Therefore, the ability to determine the correspondence between the storage elements of multiple circuits quickly and effectively has become increasingly important, especially for large and complicated circuits.
The present invention provides a method and a system of verifying two sequential circuits, a first sequential circuit and a second sequential circuit. In one embodiment, the method comprises determining storage elements of the first and second sequential circuit, selecting pairs of storage elements of the first sequential circuit, establishing distinguishing criteria from the selected pairs of storage elements of the first sequential circuit and grouping the storage elements of the first and second sequential circuits based on the distinguishing criteria. The distinguishing criteria in one embodiment comprises computing a sequence of test vectors that causes outputs of one storage element in a selected pair of storage elements to differ from outputs of other storage elements.
In another embodiment, a method of verifying a first sequential circuit and a second sequential circuit both having primary inputs and primary outputs is provided. The method comprises grouping storage elements of the first and second sequential circuits, determining next states of the storage elements of the first and second sequential circuits or determining a probabilistic hash code using abstract BDDs or partitioned BDDs or using full ROBDDs without or with hash codes, comparing the hash code or the ROBDD of next state of the storage elements of the first sequential circuits to the next states of the storage elements of the second sequential circuits and regrouping the storage elements of the first and second sequential circuits based on the equivalence of the hash code or ROBDDs of the next states of the first and second sequential circuits. In one form, determining the next states of storage elements includes building sampled Boolean decision diagrams or abstract Boolean decision diagrams to represent the next states of the storage elements.